$\forall$$T$:Type, $L$:$T$ List, $P$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$$\rightarrow\mathbb{B}$). filter2($P$;$L$) $\in$ $T$ List